T:Type, LL:(T List) List. concat(LL) = nil  T List  (LLL. L = nil  T List) 

latex

Definitions	t  T, xL. P(x), P  Q, x:A. B(x), Prop, x. t(x), P  Q, P  Q, P & Q, concat(ll), as @ bs
Lemmas	append is nil, append wf, iff functionality wrt iff, l all cons, concat wf, l all wf, l all nil